H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.926 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule List

((mapAccumR :: (c -> b -> (c,a)) -> c -> [b] -> (c,[a])) :: (c -> b -> (c,a)) -> c -> [b] -> (c,[a]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumR :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])

mapAccumR

_ s []

(s,[])

mapAccumR

f s (x : xs)

(s'',y : ys)

where

(\(s',_) ->s') vv8

s''

(\(s'',_) ->s'') vv7

vv7

f s' x

vv8

mapAccumR f s xs

(\(_,y) ->y) vv7

(\(_,ys) ->ys) vv8

module Maybe where

import qualified List
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\(_,y)→y

is transformed to

y0 (_,y) = y

The following Lambda expression

\(_,ys)→ys

is transformed to

ys0 (_,ys) = ys

The following Lambda expression

\(s'',_)→s''

is transformed to

s''0 (s'',_) = s''

The following Lambda expression

\(s',_)→s'

is transformed to

s'0 (s',_) = s'

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule List

((mapAccumR :: (c -> b -> (c,a)) -> c -> [b] -> (c,[a])) :: (c -> b -> (c,a)) -> c -> [b] -> (c,[a]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumR :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])

mapAccumR

_ s []

(s,[])

mapAccumR

f s (x : xs)

(s'',y : ys)

where

s'0 vv8

s''

s''0 vv7

s''0

(s'',_)

s''

s'0

(s',_)

vv7

f s' x

vv8

mapAccumR f s xs

y0 vv7

(_,y)

ys0 vv8

ys0

(_,ys)

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((mapAccumR :: (a -> c -> (a,b)) -> a -> [c] -> (a,[b])) :: (a -> c -> (a,b)) -> a -> [c] -> (a,[b]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumR :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])

mapAccumR

vw s []

(s,[])

mapAccumR

f s (x : xs)

(s'',y : ys)

where

s'0 vv8

s''

s''0 vv7

s''0

(s'',vz)

s''

s'0

(s',wu)

vv7

f s' x

vv8

mapAccumR f s xs

y0 vv7

(vy,y)

ys0 vv8

ys0

(vx,ys)

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule List

((mapAccumR :: (c -> a -> (c,b)) -> c -> [a] -> (c,[b])) :: (c -> a -> (c,b)) -> c -> [a] -> (c,[b]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumR :: (c -> a -> (c,b)) -> c -> [a] -> (c,[b])

mapAccumR

vw s []

(s,[])

mapAccumR

f s (x : xs)

(s'',y : ys)

where

s'0 vv8

s''

s''0 vv7

s''0

(s'',vz)

s''

s'0

(s',wu)

vv7

f s' x

vv8

mapAccumR f s xs

y0 vv7

(vy,y)

ys0 vv8

ys0

(vx,ys)

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

(s'',y : ys)

where

s' = s'0 vv8

s'' = s''0 vv7

s''0 (s'',vz) = s''

s'0 (s',wu) = s'

vv7 = f s' x

vv8 = mapAccumR f s xs

y = y0 vv7

y0 (vy,y) = y

ys = ys0 vv8

ys0 (vx,ys) = ys

are unpacked to the following functions on top level

mapAccumRY wx wy wz xu = mapAccumRY0 wx wy wz xu (mapAccumRVv7 wx wy wz xu)

mapAccumRS'' wx wy wz xu = mapAccumRS''0 wx wy wz xu (mapAccumRVv7 wx wy wz xu)

mapAccumRYs wx wy wz xu = mapAccumRYs0 wx wy wz xu (mapAccumRVv8 wx wy wz xu)

mapAccumRS''0 wx wy wz xu (s'',vz) = s''

mapAccumRY0 wx wy wz xu (vy,y) = y

mapAccumRVv8 wx wy wz xu = mapAccumR wx wy wz

mapAccumRS' wx wy wz xu = mapAccumRS'0 wx wy wz xu (mapAccumRVv8 wx wy wz xu)

mapAccumRYs0 wx wy wz xu (vx,ys) = ys

mapAccumRS'0 wx wy wz xu (s',wu) = s'

mapAccumRVv7 wx wy wz xu = wx (mapAccumRS' wx wy wz xu) xu

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

mainModule List

(mapAccumR :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a]))

module List where

import qualified Maybe
import qualified Prelude

mapAccumR :: (b -> c -> (b,a)) -> b -> [c] -> (b,[a])

mapAccumR	vw s []	=	(s,[])
mapAccumR	f s (x : xs)	=	(mapAccumRS'' f s xs x,mapAccumRY f s xs x : mapAccumRYs f s xs x)

mapAccumRS'

wx wy wz xu

mapAccumRS'0 wx wy wz xu (mapAccumRVv8 wx wy wz xu)

mapAccumRS''

wx wy wz xu

mapAccumRS''0 wx wy wz xu (mapAccumRVv7 wx wy wz xu)

mapAccumRS''0

wx wy wz xu (s'',vz)

s''

mapAccumRS'0

wx wy wz xu (s',wu)

mapAccumRVv7

wx wy wz xu

wx (mapAccumRS' wx wy wz xu) xu

mapAccumRVv8

wx wy wz xu

mapAccumR wx wy wz

mapAccumRY

wx wy wz xu

mapAccumRY0 wx wy wz xu (mapAccumRVv7 wx wy wz xu)

mapAccumRY0

wx wy wz xu (vy,y)

mapAccumRYs

wx wy wz xu

mapAccumRYs0 wx wy wz xu (mapAccumRVv8 wx wy wz xu)

mapAccumRYs0

wx wy wz xu (vx,ys)

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="mapAccumR",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="mapAccumR xv3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="mapAccumR xv3 xv4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="mapAccumR xv3 xv4 xv5",fontsize=16,color="burlywood",shape="triangle"];44[label="xv5/xv50 : xv51",fontsize=10,color="white",style="solid",shape="box"];5 -> 44[label="",style="solid", color="burlywood", weight=9];
44 -> 6[label="",style="solid", color="burlywood", weight=3];
45[label="xv5/[]",fontsize=10,color="white",style="solid",shape="box"];5 -> 45[label="",style="solid", color="burlywood", weight=9];
45 -> 7[label="",style="solid", color="burlywood", weight=3];
6[label="mapAccumR xv3 xv4 (xv50 : xv51)",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="mapAccumR xv3 xv4 []",fontsize=16,color="black",shape="box"];7 -> 9[label="",style="solid", color="black", weight=3];
8[label="(mapAccumRS'' xv3 xv4 xv51 xv50,mapAccumRY xv3 xv4 xv51 xv50 : mapAccumRYs xv3 xv4 xv51 xv50)",fontsize=16,color="green",shape="box"];8 -> 10[label="",style="dashed", color="green", weight=3];
8 -> 11[label="",style="dashed", color="green", weight=3];
8 -> 12[label="",style="dashed", color="green", weight=3];
9[label="(xv4,[])",fontsize=16,color="green",shape="box"];10[label="mapAccumRS'' xv3 xv4 xv51 xv50",fontsize=16,color="black",shape="box"];10 -> 13[label="",style="solid", color="black", weight=3];
11[label="mapAccumRY xv3 xv4 xv51 xv50",fontsize=16,color="black",shape="box"];11 -> 14[label="",style="solid", color="black", weight=3];
12[label="mapAccumRYs xv3 xv4 xv51 xv50",fontsize=16,color="black",shape="box"];12 -> 15[label="",style="solid", color="black", weight=3];
13 -> 19[label="",style="dashed", color="red", weight=0];
13[label="mapAccumRS''0 xv3 xv4 xv51 xv50 (mapAccumRVv7 xv3 xv4 xv51 xv50)",fontsize=16,color="magenta"];13 -> 20[label="",style="dashed", color="magenta", weight=3];
14 -> 24[label="",style="dashed", color="red", weight=0];
14[label="mapAccumRY0 xv3 xv4 xv51 xv50 (mapAccumRVv7 xv3 xv4 xv51 xv50)",fontsize=16,color="magenta"];14 -> 25[label="",style="dashed", color="magenta", weight=3];
15 -> 28[label="",style="dashed", color="red", weight=0];
15[label="mapAccumRYs0 xv3 xv4 xv51 xv50 (mapAccumRVv8 xv3 xv4 xv51 xv50)",fontsize=16,color="magenta"];15 -> 29[label="",style="dashed", color="magenta", weight=3];
20[label="mapAccumRVv7 xv3 xv4 xv51 xv50",fontsize=16,color="black",shape="triangle"];20 -> 22[label="",style="solid", color="black", weight=3];
19[label="mapAccumRS''0 xv3 xv4 xv51 xv50 xv6",fontsize=16,color="burlywood",shape="triangle"];49[label="xv6/(xv60,xv61)",fontsize=10,color="white",style="solid",shape="box"];19 -> 49[label="",style="solid", color="burlywood", weight=9];
49 -> 23[label="",style="solid", color="burlywood", weight=3];
25 -> 20[label="",style="dashed", color="red", weight=0];
25[label="mapAccumRVv7 xv3 xv4 xv51 xv50",fontsize=16,color="magenta"];24[label="mapAccumRY0 xv3 xv4 xv51 xv50 xv7",fontsize=16,color="burlywood",shape="triangle"];51[label="xv7/(xv70,xv71)",fontsize=10,color="white",style="solid",shape="box"];24 -> 51[label="",style="solid", color="burlywood", weight=9];
51 -> 27[label="",style="solid", color="burlywood", weight=3];
29[label="mapAccumRVv8 xv3 xv4 xv51 xv50",fontsize=16,color="black",shape="triangle"];29 -> 31[label="",style="solid", color="black", weight=3];
28[label="mapAccumRYs0 xv3 xv4 xv51 xv50 xv8",fontsize=16,color="burlywood",shape="triangle"];52[label="xv8/(xv80,xv81)",fontsize=10,color="white",style="solid",shape="box"];28 -> 52[label="",style="solid", color="burlywood", weight=9];
52 -> 32[label="",style="solid", color="burlywood", weight=3];
22[label="xv3 (mapAccumRS' xv3 xv4 xv51 xv50) xv50",fontsize=16,color="green",shape="box"];22 -> 33[label="",style="dashed", color="green", weight=3];
22 -> 34[label="",style="dashed", color="green", weight=3];
23[label="mapAccumRS''0 xv3 xv4 xv51 xv50 (xv60,xv61)",fontsize=16,color="black",shape="box"];23 -> 35[label="",style="solid", color="black", weight=3];
27[label="mapAccumRY0 xv3 xv4 xv51 xv50 (xv70,xv71)",fontsize=16,color="black",shape="box"];27 -> 36[label="",style="solid", color="black", weight=3];
31 -> 5[label="",style="dashed", color="red", weight=0];
31[label="mapAccumR xv3 xv4 xv51",fontsize=16,color="magenta"];31 -> 37[label="",style="dashed", color="magenta", weight=3];
32[label="mapAccumRYs0 xv3 xv4 xv51 xv50 (xv80,xv81)",fontsize=16,color="black",shape="box"];32 -> 38[label="",style="solid", color="black", weight=3];
33[label="mapAccumRS' xv3 xv4 xv51 xv50",fontsize=16,color="black",shape="box"];33 -> 39[label="",style="solid", color="black", weight=3];
34[label="xv50",fontsize=16,color="green",shape="box"];35[label="xv60",fontsize=16,color="green",shape="box"];36[label="xv71",fontsize=16,color="green",shape="box"];37[label="xv51",fontsize=16,color="green",shape="box"];38[label="xv81",fontsize=16,color="green",shape="box"];39 -> 40[label="",style="dashed", color="red", weight=0];
39[label="mapAccumRS'0 xv3 xv4 xv51 xv50 (mapAccumRVv8 xv3 xv4 xv51 xv50)",fontsize=16,color="magenta"];39 -> 41[label="",style="dashed", color="magenta", weight=3];
41 -> 29[label="",style="dashed", color="red", weight=0];
41[label="mapAccumRVv8 xv3 xv4 xv51 xv50",fontsize=16,color="magenta"];40[label="mapAccumRS'0 xv3 xv4 xv51 xv50 xv9",fontsize=16,color="burlywood",shape="triangle"];56[label="xv9/(xv90,xv91)",fontsize=10,color="white",style="solid",shape="box"];40 -> 56[label="",style="solid", color="burlywood", weight=9];
56 -> 42[label="",style="solid", color="burlywood", weight=3];
42[label="mapAccumRS'0 xv3 xv4 xv51 xv50 (xv90,xv91)",fontsize=16,color="black",shape="box"];42 -> 43[label="",style="solid", color="black", weight=3];
43[label="xv90",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ QDP

                      ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_mapAccumRVv8(xv3, xv4, xv51, xv50, ba, bb, bc) → new_mapAccumR(xv3, xv4, xv51, ba, bb, bc)
new_mapAccumR(xv3, xv4, :(xv50, xv51), ba, bb, bc) → new_mapAccumRVv8(xv3, xv4, xv51, xv50, ba, bb, bc)
new_mapAccumR(xv3, xv4, :(xv50, xv51), ba, bb, bc) → new_mapAccumRVv7(xv3, xv4, xv51, xv50, ba, bb, bc)
new_mapAccumR(xv3, xv4, :(xv50, xv51), ba, bb, bc) → new_mapAccumR(xv3, xv4, xv51, ba, bb, bc)
new_mapAccumRVv7(xv3, xv4, xv51, xv50, ba, bb, bc) → new_mapAccumRVv8(xv3, xv4, xv51, xv50, ba, bb, bc)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_mapAccumR(xv3, xv4, :(xv50, xv51), ba, bb, bc) → new_mapAccumRVv8(xv3, xv4, xv51, xv50, ba, bb, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 5, 5 >= 6, 6 >= 7
new_mapAccumRVv7(xv3, xv4, xv51, xv50, ba, bb, bc) → new_mapAccumRVv8(xv3, xv4, xv51, xv50, ba, bb, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 >= 6, 7 >= 7
new_mapAccumRVv8(xv3, xv4, xv51, xv50, ba, bb, bc) → new_mapAccumR(xv3, xv4, xv51, ba, bb, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 5 >= 4, 6 >= 5, 7 >= 6
new_mapAccumR(xv3, xv4, :(xv50, xv51), ba, bb, bc) → new_mapAccumR(xv3, xv4, xv51, ba, bb, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 4 >= 4, 5 >= 5, 6 >= 6
new_mapAccumR(xv3, xv4, :(xv50, xv51), ba, bb, bc) → new_mapAccumRVv7(xv3, xv4, xv51, xv50, ba, bb, bc)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 5, 5 >= 6, 6 >= 7